FDL - Nuprl Lemma : es-increasing-sequence

Nuprl Lemma : es-increasing-sequence

es:ES, m:

, f:(

m

E). (

i:

(m-1). (f(i) <loc f(i+1)))

(

i:

m, j:

i. (f(j) <loc f(i)))

Definitions , t T, x:A. B(x), AB, P & Q, i j < k, P Q, False, A, {i..j}, (e <loc e'), Prop, E, ES, , ij, P Q, Dec(P), {T}, SQType(T), Trans x,y:T. E(x;y)

Lemmas es-locl-trans, decidable int equal, ge wf, nat properties, nat wf, event system wf, nat plus wf, es-E wf, int seg wf, es-locl wf, le wf